;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "icommon.lisp")

(module MCommon
  
  
  ; takes a natural number to the powe of another natural number
  (defun pow (i power)
    (if (or (not (natp power)) (not (natp i)) (equal power 0))
        1
        (* i (pow i (- power 1)))))
  
  ; returns  the square
  (defun square (n)
    (* n n))
  
  ; checks if the value is between the min and max
  (defun InRange(value min max)
    (and (>= value min) (<= value max)))
  
  ; returns val if within the min and max, otherwise returns min if val < min or max otherwise
  (defun Cap (value min max)
    (if (< value min)
        min
        (if (> value max)
            max
            value)))
  
  ; helper for hexcalculate
  (defun hexCalc (list i)
    (if (null list)
        0
        (+ (* (car list) (pow 256 i)) (hexCalc (cdr list) (+ i 1)))))
  
  ; takes a list of byte integers and converts them to a big integer
  (defun hexCalculate (xs)
    (hexCalc xs 0))
  
  ;Givent a decimal value, returns the four byte equivalent
  (defun int->bytes (integer)
    (let* ((hex1 (logand 255 integer))
           (hex2 (/ (logand (* 255 256) integer) 256))
           (hex3 (/ (logand (* 255 256 256) integer) (* 256 256)))
           (hex4 (/ (logand (* 255 256 256 256) integer) (* 256 256 256))))
      (list hex1 hex2 hex3 hex4)))
  
  ;Size = 54(header) + Width*Height*3 (RGB for each pixel) + (Width%4)*Height (Padding)
  (defun GetBMPSize(width height)
    (+ 54 (* width height 3) (* (mod width 4) height)))
    
  ;Get all the elements in the list AFTER the nth element
  (defun remainingElements (list n)
    (if (equal n 1)
        (cdr list)
        (remainingElements (cdr list) (- n 1))))
  
  ;Get the nth element in the list
  (defun getElement (list n)
    (if (equal n 1)
        (car list)
        (getElement (cdr list) (- n 1))))
  
  (defun getLastElement(list)
    (if (consp (cdr list))
        (getLastElement (cdr list))
        (car list)))
        
  
  ;Gets the next 'count' elements.
  (defun getNextElements(aList count)
    (if (<= count 1)
        (list (car aList))
        (append (list (car aList)) (getNextElements (cdr aList) (- count 1)))))
  
    ;Get the elements in aList between the start and end indecies (inclusive
  (defun getElements (aList start end)
    (if (<= start 1)
        (getNextElements aList end)
        (getElements (cdr aList) (- start 1) (- end 1))))
  
  
;  ;Get the elements in aList between the start and end indecies
;  (defun getElements (aList start end)
;    (if (<= end start)
;        (list (car aList))
;        (append (list (car aList)) (getElements (cdr aList) (+ start 1) end))))
  
  ; Checks if the color is between 0 and 255
  (defun validColor (color)
    (and (natp color ) (< color 256) (>= color 0)))
  
  ; checks if each of the three elements of a list is between 0 and 255
  (defun validPixel (pixel)
    (and (integer-listp pixel) (equal (len pixel) 3) (validColor (getElement pixel 1)) (validColor (getElement pixel 2)) (validColor (getElement pixel 3))))
  
  ; checks if the x and y value are within the image
  (defun validPoint (x y width height)
      (and (natp x) (natp y) (natp width) (natp height)
           (> x 0) (<= x width)
           (> y 0) (<= y height)
           ))
  
  ;checks if both points are within the image and point 1 is less then point 2
  (defun validPair (x1 y1 x2 y2 width height)
    (and (validPoint x1 y1 width height)
         (validPoint x2 y2 width height)
         (<= x1 x2)
         (<= y1 y2)))
  
  (export ICommon))